WebAssembly 形式手法
WebAssembyは
Isabelle/HOL
で
well-defined
に定義されている
$ ^{(1)}
ソースは↓に
WebAssembly - Archive of Formal Proofs
. 2018-04-29
Coqの方でやっているものもある
GitHub:
WasmCert/WasmCert-Coq: A mechanisation of Wasm in Coq
今はCoqで形式化している？
WebAssembly関連の論文
『Formal Methods and the WebAssembly Specification』
. 2019.
『Mechanising and Verifying the WebAssembly Specification』
Two Mechanisations of WebAssembly 1.0 | SpringerLink
確認用
Q. WebAssembly 形式手法
参考
(1)
『Formal Methods and the WebAssembly Specification』
『Mechanising and Verifying the WebAssembly Specification』
関連
Isabelle